主要經歷
1976-1978福建寧德地區民族中學
1978-1979北京大學
1979-1988挪威奧斯陸大學
1986-1986挪威INENCO公司
1987-1987挪威奧斯陸大學
1988-1989中科院軟體所
1989-1989香港Citibank公司
1989-1991挪威奧斯陸大學
1991-1993挪威Telemark學院
1993-1994中科院軟體所
1994-1995挪威Telemark學院
1995-1997挪威Achilles公司
1997-2001挪威能源技術研究所
2001-2004中科院軟體所
研究成果
主要從事形式化方法及相關領域的研究，在程式的形式驗證、邏輯推理、模型檢測、軟體系統設計方法的形式化等方面有一定的研究積累。在自動推理的研究方面，對謂詞公式中的量詞和其它邏輯聯結詞作了詳細的分析。區分了引理中它們的使用對證明的複雜性的不同影響。在這基礎上分析了連線法和消解法及其變種與可自由使用引理的邏輯系統的關係，論證了這些方法在引理使用上的不同的局限性，加深了對自動定理證明方法的不足的認識，並揭示了擴展的消解法，即允許表示定義的重言子句集合加到初始子句集合進行消解，其功能實質上就是為了增加複雜引理套用的可能性，以提高推理效率。在這些工作的基礎上，提出了一個分析模型個數的算法和一個命題邏輯公式判定的算法，取得了良好的理論效果。這方面的工作對認識自動定理證明的困難本質和命題邏輯公式判定算法的研究起到了一定的推動作用。在模型檢測的研究方面，將模型檢測方法套用於操作程式的驗證，提出了多種針對具體套用做抽象和分不同情況以降低模型檢測空間和時間複雜性的方法，包括將操作程式和操作環境的模型用中間進程分開，遞增式地對操作環境進行建模和逐級驗證以降低模型檢測的套用門檻；基於對套用目標和模型的分析，將套用領域的特殊性質嵌入到模型及性質描述中以降低模型檢測的複雜性；結合對模型的靜態分析，將所選的不同情況嵌入到性質描述中以降低模型檢測的複雜性。這方面的工作對模型檢測在不同領域的套用有一定的借鑑作用。
獲獎情況
1993年獲王寬誠科研獎金資助。
2002年獲財政部中科院引進國外傑出人才資助。
